Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix: Spurious message of checkerpool already disposed. #937

Closed
wants to merge 3 commits into from
Closed

Fix: Spurious message of checkerpool already disposed. #937

wants to merge 3 commits into from

Conversation

MikaelMayer
Copy link
Collaborator

@MikaelMayer MikaelMayer commented Aug 13, 2024 •
edited
Loading

Looking at the CI result of https://github.com/dafny-lang/dafny/actions/runs/10330235840/job/28615735562?pr=5675, I see like often:

System.Exception: CheckerPool was already disposed
         at VC.CheckerPool.FindCheckerFor(Program program, Split split, CancellationToken cancellationToken)
         at Microsoft.Boogie.VerificationTask.StartRun(CancellationToken cancellationToken)+MoveNext()
         at Microsoft.Boogie.VerificationTask.StartRun(CancellationToken

This PR hopefully fixes this message.

Rationale.

This message does not seem to cause any trouble whatsoever, it's just that the exception is never caught.
Since at the call site, there is a catch of OperationCanceledException, I piggy back on this exception to return it instead of a generic exception, so that the control flow will not display this exception anymore.

I don't know of a way to test this PR, but we will see if the already disposed messages in PR CI disappear.

@MikaelMayer
Fix: Spurious message of checkerpool already disposed.
44f0dff 
Looking at the CI result of https://github.com/dafny-lang/dafny/actions/runs/10330235840/job/28615735562?pr=5675, I see like often:
```
System.Exception: CheckerPool was already disposed
         at VC.CheckerPool.FindCheckerFor(Program program, Split split, CancellationToken cancellationToken)
         at Microsoft.Boogie.VerificationTask.StartRun(CancellationToken cancellationToken)+MoveNext()
         at Microsoft.Boogie.VerificationTask.StartRun(CancellationToken
```
This PR hopefully fixes this message
keyboardDrummer
keyboardDrummer requested changes Aug 13, 2024
View reviewed changes
Copy link
Collaborator

@keyboardDrummer keyboardDrummer left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't we prevent the exception from being thrown in the first place?

Since at the call site, there is a catch of OperationCanceledException, I piggy back on this exception to return it instead of a generic exception, so that the control flow will not display this exception anymore.

That sounds like it would need a comment both where you throw and where you catch the exception, but better would be not to piggyback on OperationCanceledException.

@MikaelMayer
Copy link
Collaborator Author

from

We really have a nasty concurrency issue here, and even I am not sure of my fix. Before any brittleness issue on the LSP, I almost always saw one of these message. But I don't know if they always appear or just during errors.

If you wanted to get rid of the exception, you'd have to ensure that FindCheckerFor is never called when disposed is true, or remove the exception while ensuring everything goes as planned. The first case is not possible, because the only thing that can turn dispose to true is the method Dispose(), and that method is called only if Engine.Dispose() is called, which according to the Dafny source code, can be called at any moment.

Now if you remove the exception and disposed is true,, you'll enter checkersSemaphore.WaitAsync(cancellationToken), and since all threads should have been cancelled, you'll end with nothing in availableCheckers, so one new checker will be created and returned, although that's useless. Could it lead to memory leaks? I don't know.

What's your take on all of this information?

@keyboardDrummer
Copy link
Collaborator

Made a PR that might resolve the issue: #941

@keyboardDrummer keyboardDrummer mentioned this pull request Aug 16, 2024
Merged
@MikaelMayer
Copy link
Collaborator Author

Made a PR that might resolve the issue: #941

You're the best. Closing this one then and I'll post my review on yours because it seem like it does the right thing.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@keyboardDrummer keyboardDrummer keyboardDrummer requested changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@MikaelMayer @keyboardDrummer